<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>索引</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/vfa.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 3: 函数式算法验证</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<table>
<tr>
<td>Global Index</td>
<td><a href="coqindex.html#global_A">A</a></td>
<td><a href="coqindex.html#global_B">B</a></td>
<td><a href="coqindex.html#global_C">C</a></td>
<td><a href="coqindex.html#global_D">D</a></td>
<td><a href="coqindex.html#global_E">E</a></td>
<td><a href="coqindex.html#global_F">F</a></td>
<td><a href="coqindex.html#global_G">G</a></td>
<td><a href="coqindex.html#global_H">H</a></td>
<td><a href="coqindex.html#global_I">I</a></td>
<td>J</td>
<td><a href="coqindex.html#global_K">K</a></td>
<td><a href="coqindex.html#global_L">L</a></td>
<td><a href="coqindex.html#global_M">M</a></td>
<td><a href="coqindex.html#global_N">N</a></td>
<td><a href="coqindex.html#global_O">O</a></td>
<td><a href="coqindex.html#global_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#global_R">R</a></td>
<td><a href="coqindex.html#global_S">S</a></td>
<td><a href="coqindex.html#global_T">T</a></td>
<td><a href="coqindex.html#global_U">U</a></td>
<td><a href="coqindex.html#global_V">V</a></td>
<td><a href="coqindex.html#global_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="coqindex.html#global_Z">Z</a></td>
<td><a href="coqindex.html#global_:">:</a></td>
<td>_</td>
<td>(617 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#notation_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#notation_S">S</a></td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td><a href="coqindex.html#notation_:">:</a></td>
<td>_</td>
<td>(5 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td>A</td>
<td><a href="coqindex.html#module_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="coqindex.html#module_E">E</a></td>
<td><a href="coqindex.html#module_F">F</a></td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#module_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#module_L">L</a></td>
<td><a href="coqindex.html#module_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="coqindex.html#module_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#module_R">R</a></td>
<td><a href="coqindex.html#module_S">S</a></td>
<td><a href="coqindex.html#module_T">T</a></td>
<td>U</td>
<td><a href="coqindex.html#module_V">V</a></td>
<td><a href="coqindex.html#module_W">W</a></td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(27 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
<td><a href="coqindex.html#variable_A">A</a></td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#variable_S">S</a></td>
<td><a href="coqindex.html#variable_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(13 entries)</td>
</tr>
<tr>
<td>Library Index</td>
<td><a href="coqindex.html#library_A">A</a></td>
<td><a href="coqindex.html#library_B">B</a></td>
<td><a href="coqindex.html#library_C">C</a></td>
<td><a href="coqindex.html#library_D">D</a></td>
<td><a href="coqindex.html#library_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="coqindex.html#library_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="coqindex.html#library_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#library_R">R</a></td>
<td><a href="coqindex.html#library_S">S</a></td>
<td><a href="coqindex.html#library_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(14 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
<td><a href="coqindex.html#lemma_A">A</a></td>
<td><a href="coqindex.html#lemma_B">B</a></td>
<td><a href="coqindex.html#lemma_C">C</a></td>
<td><a href="coqindex.html#lemma_D">D</a></td>
<td><a href="coqindex.html#lemma_E">E</a></td>
<td><a href="coqindex.html#lemma_F">F</a></td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#lemma_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#lemma_L">L</a></td>
<td><a href="coqindex.html#lemma_M">M</a></td>
<td><a href="coqindex.html#lemma_N">N</a></td>
<td>O</td>
<td><a href="coqindex.html#lemma_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#lemma_R">R</a></td>
<td><a href="coqindex.html#lemma_S">S</a></td>
<td><a href="coqindex.html#lemma_T">T</a></td>
<td><a href="coqindex.html#lemma_U">U</a></td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="coqindex.html#lemma_Z">Z</a></td>
<td>_</td>
<td>(211 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#axiom_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#axiom_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td><a href="coqindex.html#axiom_P">P</a></td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#axiom_S">S</a></td>
<td><a href="coqindex.html#axiom_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(37 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
<td><a href="coqindex.html#constructor_A">A</a></td>
<td><a href="coqindex.html#constructor_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="coqindex.html#constructor_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#constructor_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#constructor_L">L</a></td>
<td>M</td>
<td><a href="coqindex.html#constructor_N">N</a></td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td><a href="coqindex.html#constructor_R">R</a></td>
<td><a href="coqindex.html#constructor_S">S</a></td>
<td><a href="coqindex.html#constructor_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(52 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
<td><a href="coqindex.html#inductive_A">A</a></td>
<td><a href="coqindex.html#inductive_B">B</a></td>
<td><a href="coqindex.html#inductive_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#inductive_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#inductive_L">L</a></td>
<td>M</td>
<td><a href="coqindex.html#inductive_N">N</a></td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#inductive_S">S</a></td>
<td><a href="coqindex.html#inductive_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(26 entries)</td>
</tr>
<tr>
<td>Section Index</td>
<td><a href="coqindex.html#section_A">A</a></td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#section_S">S</a></td>
<td><a href="coqindex.html#section_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(6 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
<td><a href="coqindex.html#definition_A">A</a></td>
<td><a href="coqindex.html#definition_B">B</a></td>
<td><a href="coqindex.html#definition_C">C</a></td>
<td><a href="coqindex.html#definition_D">D</a></td>
<td><a href="coqindex.html#definition_E">E</a></td>
<td><a href="coqindex.html#definition_F">F</a></td>
<td><a href="coqindex.html#definition_G">G</a></td>
<td><a href="coqindex.html#definition_H">H</a></td>
<td><a href="coqindex.html#definition_I">I</a></td>
<td>J</td>
<td><a href="coqindex.html#definition_K">K</a></td>
<td><a href="coqindex.html#definition_L">L</a></td>
<td><a href="coqindex.html#definition_M">M</a></td>
<td><a href="coqindex.html#definition_N">N</a></td>
<td><a href="coqindex.html#definition_O">O</a></td>
<td><a href="coqindex.html#definition_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#definition_R">R</a></td>
<td><a href="coqindex.html#definition_S">S</a></td>
<td><a href="coqindex.html#definition_T">T</a></td>
<td><a href="coqindex.html#definition_U">U</a></td>
<td><a href="coqindex.html#definition_V">V</a></td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(226 entries)</td>
</tr>
</table>
<hr/>
<h1>Global Index</h1>
<a name="global_A"></a><h2>A </h2>
<a href="VFA.SearchTree.html#Abs">Abs</a> [inductive, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#Abs">Abs</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#Abs">Abs</a> [inductive, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#abstract">abstract</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#abstraction_of_bogus_tree">abstraction_of_bogus_tree</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#AbsX">AbsX</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#Abs_E">Abs_E</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#Abs_E">Abs_E</a> [constructor, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#Abs_helper">Abs_helper</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#Abs_T">Abs_T</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#Abs_T">Abs_T</a> [constructor, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#Abs_three_ten">Abs_three_ten</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Color.html#add_edge">add_edge</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#adj">adj</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#adj_ext">adj_ext</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="ADT.html">ADT</a> [library]<br/>
<a href="VFA.ADT.html#ADT_SUMMARY">ADT_SUMMARY</a> [section, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#ADT_SUMMARY.default">ADT_SUMMARY.default</a> [variable, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#ADT_SUMMARY.V">ADT_SUMMARY.V</a> [variable, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="global_B"></a><h2>B </h2>
<a href="VFA.Redblack.html#balance">balance</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#balance_relate">balance_relate</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#balance_SearchTree">balance_SearchTree</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#balance_SearchTree">balance_SearchTree</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#balance_SearchTree">balance_SearchTree</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="Binom.html">Binom</a> [library]<br/>
<a href="VFA.Binom.html#BinomQueue">BinomQueue</a> [module, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.Abs">BinomQueue.Abs</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.abs_perm">BinomQueue.abs_perm</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.can_relate">BinomQueue.can_relate</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.carry">BinomQueue.carry</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.carry_elems">BinomQueue.carry_elems</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.carry_valid">BinomQueue.carry_valid</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max">BinomQueue.delete_max</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_aux">BinomQueue.delete_max_aux</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_None_relate">BinomQueue.delete_max_None_relate</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_Some_priq">BinomQueue.delete_max_Some_priq</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_Some_relate">BinomQueue.delete_max_Some_relate</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.empty">BinomQueue.empty</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.empty_priq">BinomQueue.empty_priq</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.empty_relate">BinomQueue.empty_relate</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.find_max">BinomQueue.find_max</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.find_max'">BinomQueue.find_max'</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.heap_delete_max">BinomQueue.heap_delete_max</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.insert">BinomQueue.insert</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.insert_priq">BinomQueue.insert_priq</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.insert_relate">BinomQueue.insert_relate</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.join">BinomQueue.join</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.join_elems">BinomQueue.join_elems</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.join_valid">BinomQueue.join_valid</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.key">BinomQueue.key</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.Leaf">BinomQueue.Leaf</a> [constructor, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.manual_grade_for_priqueue_elems">BinomQueue.manual_grade_for_priqueue_elems</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.merge">BinomQueue.merge</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.merge_priq">BinomQueue.merge_priq</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.merge_relate">BinomQueue.merge_relate</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.Node">BinomQueue.Node</a> [constructor, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.pow2heap">BinomQueue.pow2heap</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.pow2heap'">BinomQueue.pow2heap'</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priq">BinomQueue.priq</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priqueue">BinomQueue.priqueue</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priqueue_elems">BinomQueue.priqueue_elems</a> [inductive, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priqueue_elems_ext">BinomQueue.priqueue_elems_ext</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priq'">BinomQueue.priq'</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.smash">BinomQueue.smash</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.smash_elems">BinomQueue.smash_elems</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.smash_valid">BinomQueue.smash_valid</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree">BinomQueue.tree</a> [inductive, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_can_relate">BinomQueue.tree_can_relate</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems">BinomQueue.tree_elems</a> [inductive, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems_ext">BinomQueue.tree_elems_ext</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems_leaf">BinomQueue.tree_elems_leaf</a> [constructor, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems_node">BinomQueue.tree_elems_node</a> [constructor, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_perm">BinomQueue.tree_perm</a> [lemma, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.unzip">BinomQueue.unzip</a> [definition, in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Redblack.html#Black">Black</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="global_C"></a><h2>C </h2>
<a href="VFA.SearchTree.html#can_relate">can_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#cardinal_map">cardinal_map</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#check_example_map">check_example_map</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#check_too_clever">check_too_clever</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#color">color</a> [inductive, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Color.html#color">color</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="Color.html">Color</a> [library]<br/>
<a href="VFA.Color.html#coloring">coloring</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#coloring_ok">coloring_ok</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#colors_of">colors_of</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#color1">color1</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#color_correct">color_correct</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Redblack.html#combine">combine</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#combine">combine</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Decide.html#compute_with_lt_dec">compute_with_lt_dec</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#compute_with_StdLib_lt_dec">compute_with_StdLib_lt_dec</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.ADT.html#cons_relate">cons_relate</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Multiset.html#contents">contents</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#contents_in">contents_in</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#contents_perm">contents_perm</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#contents_perm_aux">contents_perm_aux</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.ADT.html#create_relate">create_relate</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="global_D"></a><h2>D </h2>
<a href="Decide.html">Decide</a> [library]<br/>
<a href="VFA.Multiset.html#delete_contents">delete_contents</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Color.html#domain_example_map">domain_example_map</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="global_E"></a><h2>E </h2>
<a href="VFA.SearchTree.html#E">E</a> [constructor, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#E">E</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Color.html#E">E</a> [module, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Redblack.html#elements">elements</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#elements">elements</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#elements'">elements'</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#elements'">elements'</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#elements_property">elements_property</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#elements_relate">elements_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#elements_relate">elements_relate</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#elements_relate">elements_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#elements_relateX">elements_relateX</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#elements_relate_second_attempt">elements_relate_second_attempt</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#elements_slow_elements">elements_slow_elements</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#empty">empty</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Multiset.html#empty">empty</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#empty_is_trie">empty_is_trie</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#empty_relate">empty_relate</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#empty_tree">empty_tree</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#empty_tree">empty_tree</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#empty_tree_relate">empty_tree_relate</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#empty_tree_relate">empty_tree_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#empty_tree_SearchTree">empty_tree_SearchTree</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#empty_tree_SearchTree">empty_tree_SearchTree</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Perm.html#eqb_reflect">eqb_reflect</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Color.html#eqlistA_Eeq_eq">eqlistA_Eeq_eq</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#equivlistA_example">equivlistA_example</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#example_map">example_map</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#example_map">example_map</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#example_SearchTree_bad">example_SearchTree_bad</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#example_SearchTree_good">example_SearchTree_good</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#example_tree">example_tree</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#expand_range_SearchTree'">expand_range_SearchTree'</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Extract.html#Experiments">Experiments</a> [module, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.E">Experiments.E</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.empty_tree">Experiments.empty_tree</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.insert">Experiments.insert</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.lookup">Experiments.lookup</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.T">Experiments.T</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Perm.html#Exploration1">Exploration1</a> [module, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.bogus_subtraction">Exploration1.bogus_subtraction</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.butterfly">Exploration1.butterfly</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.first_le_second">Exploration1.first_le_second</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.manual_grade_for_Permutation_properties">Exploration1.manual_grade_for_Permutation_properties</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap">Exploration1.maybe_swap</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_correct">Exploration1.maybe_swap_correct</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_idempotent">Exploration1.maybe_swap_idempotent</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_idempotent">Exploration1.maybe_swap_idempotent</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_idempotent'">Exploration1.maybe_swap_idempotent'</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_perm">Exploration1.maybe_swap_perm</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_123">Exploration1.maybe_swap_123</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_321">Exploration1.maybe_swap_321</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.not_a_permutation">Exploration1.not_a_permutation</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.omega_example1">Exploration1.omega_example1</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.omega_example1">Exploration1.omega_example1</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.omega_example2">Exploration1.omega_example2</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.permut_example">Exploration1.permut_example</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="Extract.html">Extract</a> [library]<br/>
<br/><br/><a name="global_F"></a><h2>F </h2>
<a href="VFA.Trie.html#FastEnough">FastEnough</a> [module, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#FastEnough.collisions">FastEnough.collisions</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#FastEnough.collisions_pi">FastEnough.collisions_pi</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#FastEnough.loop">FastEnough.loop</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.ADT.html#fib">fib</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#fibish">fibish</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#fibish_correct">fibish_correct</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#fibonacci">fibonacci</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Color.html#filter_sortE">filter_sortE</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#fold_right_rev_left">fold_right_rev_left</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#forall_nodes">forall_nodes</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Sort.html#Forall_nth">Forall_nth</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Perm.html#Forall_perm">Forall_perm</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<br/><br/><a name="global_G"></a><h2>G </h2>
<a href="VFA.Color.html#G">G</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#graph">graph</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="global_H"></a><h2>H </h2>
<a href="VFA.Redblack.html#how_many_subgoals_remaining">how_many_subgoals_remaining</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="global_I"></a><h2>I </h2>
<a href="VFA.Color.html#InA_example">InA_example</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#InA_map_fst_key">InA_map_fst_key</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Redblack.html#ins">ins</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#ins">ins</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#insert">insert</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#insert">insert</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#insert">insert</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Sort.html#insert">insert</a> [definition, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Multiset.html#insertion_sort_correct">insertion_sort_correct</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Sort.html#insertion_sort_correct">insertion_sort_correct</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Multiset.html#insert_contents">insert_contents</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Redblack.html#insert_is_redblack">insert_is_redblack</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#insert_is_trie">insert_is_trie</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Sort.html#insert_perm">insert_perm</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Trie.html#insert_relate">insert_relate</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#insert_relate">insert_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#insert_relate">insert_relate</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#insert_relate'">insert_relate'</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#insert_SearchTree">insert_SearchTree</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#insert_SearchTree">insert_SearchTree</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Sort.html#insert_sorted">insert_sorted</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#insert_sorted'">insert_sorted'</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Redblack.html#ins_is_redblack">ins_is_redblack</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_not_E">ins_not_E</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_not_E">ins_not_E</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_not_E">ins_not_E</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_relate">ins_relate</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_SearchTree">ins_SearchTree</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Extract.html#int">int</a> [axiom, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Trie.html#Integers">Integers</a> [module, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.add">Integers.add</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.addc">Integers.addc</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.addc_correct">Integers.addc_correct</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.add_correct">Integers.add_correct</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.compare">Integers.compare</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.compare_correct">Integers.compare_correct</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.comparison">Integers.comparison</a> [inductive, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Eq">Integers.Eq</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Gt">Integers.Gt</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Lt">Integers.Lt</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.positive">Integers.positive</a> [inductive, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.positive2nat">Integers.positive2nat</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.positive2nat_pos">Integers.positive2nat_pos</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.print_in_binary">Integers.print_in_binary</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.succ">Integers.succ</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.succ_correct">Integers.succ_correct</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.ten">Integers.ten</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.xH">Integers.xH</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.xI">Integers.xI</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.xO">Integers.xO</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Z">Integers.Z</a> [inductive, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Zneg">Integers.Zneg</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Zpos">Integers.Zpos</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Z0">Integers.Z0</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.:::x_'~'_'0'">Integers.:::x_'~'_'0'</a> [notation, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.:::x_'~'_'1'">Integers.:::x_'~'_'1'</a> [notation, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Extract.html#IntMaps">IntMaps</a> [module, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.total_map">IntMaps.total_map</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_empty">IntMaps.t_empty</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update">IntMaps.t_update</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update_eq">IntMaps.t_update_eq</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update_neq">IntMaps.t_update_neq</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update_shadow">IntMaps.t_update_shadow</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#int2Z">int2Z</a> [axiom, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#int_ltb_reflect">int_ltb_reflect</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Color.html#in_colors_of_1">in_colors_of_1</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#In_decidable">In_decidable</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Multiset.html#in_perm_delete">in_perm_delete</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Decide.html#in_4_pi">in_4_pi</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Redblack.html#IsRB_b">IsRB_b</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#IsRB_leaf">IsRB_leaf</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#IsRB_r">IsRB_r</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Sort.html#is_a_sorting_algorithm">is_a_sorting_algorithm</a> [definition, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#is_a_sorting_algorithm">is_a_sorting_algorithm</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Multiset.html#is_a_sorting_algorithm'">is_a_sorting_algorithm'</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Redblack.html#is_redblack">is_redblack</a> [inductive, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#is_redblack_toblack">is_redblack_toblack</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#is_trie">is_trie</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="global_K"></a><h2>K </h2>
<a href="VFA.Redblack.html#key">key</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#key">key</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="global_L"></a><h2>L </h2>
<a href="VFA.ADT.html#L">L</a> [module, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Trie.html#Leaf">Leaf</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Perm.html#leb_reflect">leb_reflect</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.ADT.html#LISTISH">LISTISH</a> [module, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH.cons">LISTISH.cons</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH.create">LISTISH.create</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH.list">LISTISH.list</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH.nth">LISTISH.nth</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.SearchTree.html#list2map">list2map</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#list2map_app_left">list2map_app_left</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#list2map_app_right">list2map_app_right</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#list2map_not_in_default">list2map_not_in_default</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Multiset.html#list_delete">list_delete</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Decide.html#list_nat_eq_dec">list_nat_eq_dec</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#list_nat_in">list_nat_in</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue">List_Priqueue</a> [module, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.Abs">List_Priqueue.Abs</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.Abs'">List_Priqueue.Abs'</a> [inductive, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.Abs_intro">List_Priqueue.Abs_intro</a> [constructor, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.abs_perm">List_Priqueue.abs_perm</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.can_relate">List_Priqueue.can_relate</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max">List_Priqueue.delete_max</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max_None_relate">List_Priqueue.delete_max_None_relate</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max_Some_priq">List_Priqueue.delete_max_Some_priq</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max_Some_relate">List_Priqueue.delete_max_Some_relate</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.empty">List_Priqueue.empty</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.empty_priq">List_Priqueue.empty_priq</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.empty_relate">List_Priqueue.empty_relate</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.insert">List_Priqueue.insert</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.insert_priq">List_Priqueue.insert_priq</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.insert_relate">List_Priqueue.insert_relate</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.key">List_Priqueue.key</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.merge">List_Priqueue.merge</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.merge_priq">List_Priqueue.merge_priq</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.merge_relate">List_Priqueue.merge_relate</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.priq">List_Priqueue.priq</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.priqueue">List_Priqueue.priqueue</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select">List_Priqueue.select</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select_biggest">List_Priqueue.select_biggest</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select_biggest_aux">List_Priqueue.select_biggest_aux</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select_perm">List_Priqueue.select_perm</a> [lemma, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Trie.html#look">look</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#lookup">lookup</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#lookup">lookup</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#lookup">lookup</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#lookup_relate">lookup_relate</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#lookup_relate">lookup_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#lookup_relate">lookup_relate</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#lookup_relateX">lookup_relateX</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#lookup_relate'">lookup_relate'</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#look_ins_other">look_ins_other</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#look_ins_same">look_ins_same</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#look_leaf">look_leaf</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Color.html#low_deg">low_deg</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Extract.html#ltb">ltb</a> [axiom, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#ltb_lt">ltb_lt</a> [axiom, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Perm.html#ltb_reflect">ltb_reflect</a> [lemma, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Color.html#lt_proper">lt_proper</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#lt_strict">lt_strict</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#L.cons">L.cons</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#L.create">L.create</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#L.list">L.list</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#L.nth">L.nth</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#L_Abs">L_Abs</a> [inductive, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="global_M"></a><h2>M </h2>
<a href="VFA.Color.html#M">M</a> [module, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Redblack.html#makeBlack">makeBlack</a> [definition, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#makeblack_fiddle">makeblack_fiddle</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#makeBlack_relate">makeBlack_relate</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#manual_grade_for_elements_relate_informal">manual_grade_for_elements_relate_informal</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Multiset.html#manual_grade_for_permutations_vs_multiset">manual_grade_for_permutations_vs_multiset</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#manual_grade_for_successor_of_Z_constant_time">manual_grade_for_successor_of_Z_constant_time</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.ADT.html#MapsTable">MapsTable</a> [module, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.default">MapsTable.default</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.empty">MapsTable.empty</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.gempty">MapsTable.gempty</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.get">MapsTable.get</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.gso">MapsTable.gso</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.gss">MapsTable.gss</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.key">MapsTable.key</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.set">MapsTable.set</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.table">MapsTable.table</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.V">MapsTable.V</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Color.html#Mdomain">Mdomain</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#mk_graph">mk_graph</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Mremove_cardinal_less">Mremove_cardinal_less</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Mremove_elements">Mremove_elements</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Multiset.html#multiset">multiset</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="Multiset.html">Multiset</a> [library]<br/>
<a href="VFA.Multiset.html#multiset_delete">multiset_delete</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<br/><br/><a name="global_N"></a><h2>N </h2>
<a href="VFA.SearchTree.html#naive_lookup_relateX">naive_lookup_relateX</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#nat2pos">nat2pos</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#nat2pos2nat">nat2pos2nat</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#nat2pos_injective">nat2pos_injective</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#nearly_redblack">nearly_redblack</a> [inductive, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Color.html#node">node</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Trie.html#Node">Node</a> [constructor, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Color.html#nodemap">nodemap</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#nodes">nodes</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#nodeset">nodeset</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#not_elements_relate">not_elements_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#not_naive_lookup_relateX">not_naive_lookup_relateX</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#no_selfloop">no_selfloop</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Redblack.html#nrRB_b">nrRB_b</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#nrRB_r">nrRB_r</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.ADT.html#nth_firstn">nth_firstn</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#nth_relate">nth_relate</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="global_O"></a><h2>O </h2>
<a href="VFA.Selection.html#out_of_gas">out_of_gas</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.ADT.html#O_Abs">O_Abs</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="global_P"></a><h2>P </h2>
<a href="VFA.Color.html#palette">palette</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="Perm.html">Perm</a> [library]<br/>
<a href="VFA.Multiset.html#perm_contents">perm_contents</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#pos2nat">pos2nat</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#pos2nat2pos">pos2nat2pos</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#pos2nat_injective">pos2nat_injective</a> [lemma, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="Preface.html">Preface</a> [library]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE">PRIQUEUE</a> [module, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="Priqueue.html">Priqueue</a> [library]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.Abs">PRIQUEUE.Abs</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.abs_perm">PRIQUEUE.abs_perm</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.can_relate">PRIQUEUE.can_relate</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max">PRIQUEUE.delete_max</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max_None_relate">PRIQUEUE.delete_max_None_relate</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max_Some_priq">PRIQUEUE.delete_max_Some_priq</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max_Some_relate">PRIQUEUE.delete_max_Some_relate</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.empty">PRIQUEUE.empty</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.empty_priq">PRIQUEUE.empty_priq</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.empty_relate">PRIQUEUE.empty_relate</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.insert">PRIQUEUE.insert</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.insert_priq">PRIQUEUE.insert_priq</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.insert_relate">PRIQUEUE.insert_relate</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.key">PRIQUEUE.key</a> [definition, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.merge">PRIQUEUE.merge</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.merge_priq">PRIQUEUE.merge_priq</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.merge_relate">PRIQUEUE.merge_relate</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.priq">PRIQUEUE.priq</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.priqueue">PRIQUEUE.priqueue</a> [axiom, in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Color.html#Proper_eq_eq">Proper_eq_eq</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Proper_eq_key_elt">Proper_eq_key_elt</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="global_R"></a><h2>R </h2>
<a href="VFA.Trie.html#RatherSlow">RatherSlow</a> [module, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.collisions">RatherSlow.collisions</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.collisions_pi">RatherSlow.collisions_pi</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.empty">RatherSlow.empty</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.loop">RatherSlow.loop</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.total_mapz">RatherSlow.total_mapz</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.update">RatherSlow.update</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#Red">Red</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="Redblack.html">Redblack</a> [library]<br/>
<a href="VFA.Perm.html#reflect_example1">reflect_example1</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#reflect_example2">reflect_example2</a> [definition, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Color.html#remove_node">remove_node</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#repeat">repeat</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#repeat_step_relate">repeat_step_relate</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="global_S"></a><h2>S </h2>
<a href="VFA.Color.html#S">S</a> [module, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Multiset.html#same_contents_iff_perm">same_contents_iff_perm</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Color.html#same_mod_10">same_mod_10</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Decide.html#ScratchPad">ScratchPad</a> [module, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.greater23">ScratchPad.greater23</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.is_3_less_7">ScratchPad.is_3_less_7</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.left">ScratchPad.left</a> [constructor, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.less37">ScratchPad.less37</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.lt_dec">ScratchPad.lt_dec</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.lt_dec'">ScratchPad.lt_dec'</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.lt_dec_equivalent">ScratchPad.lt_dec_equivalent</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.right">ScratchPad.right</a> [constructor, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.sumbool">ScratchPad.sumbool</a> [inductive, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.t1">ScratchPad.t1</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.t2">ScratchPad.t2</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.t4">ScratchPad.t4</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v1a">ScratchPad.v1a</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v1b">ScratchPad.v1b</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v2a">ScratchPad.v2a</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v3">ScratchPad.v3</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.::type_scope:'{'_x_'}'_'+'_'{'_x_'}'">ScratchPad.::type_scope:'{'_x_'}'_'+'_'{'_x_'}'</a> [notation, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2">ScratchPad2</a> [module, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.insert">ScratchPad2.insert</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.insert_sorted">ScratchPad2.insert_sorted</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.le_dec">ScratchPad2.le_dec</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.lt_dec">ScratchPad2.lt_dec</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.lt_dec_axiom_1">ScratchPad2.lt_dec_axiom_1</a> [axiom, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.lt_dec_axiom_2">ScratchPad2.lt_dec_axiom_2</a> [axiom, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.max_with_axiom">ScratchPad2.max_with_axiom</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.prove_with_max_axiom">ScratchPad2.prove_with_max_axiom</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sort">ScratchPad2.sort</a> [definition, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted">ScratchPad2.sorted</a> [inductive, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted_cons">ScratchPad2.sorted_cons</a> [constructor, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted_nil">ScratchPad2.sorted_nil</a> [constructor, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted_1">ScratchPad2.sorted_1</a> [constructor, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.SearchTree.html#SearchTree">SearchTree</a> [inductive, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#SearchTree">SearchTree</a> [inductive, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="SearchTree.html">SearchTree</a> [library]<br/>
<a href="VFA.SearchTree.html#SearchTreeX">SearchTreeX</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#SearchTree'">SearchTree'</a> [inductive, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#SearchTree'">SearchTree'</a> [inductive, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#SearchTree'_le">SearchTree'_le</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#SearchTree'_le">SearchTree'_le</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Extract.html#SearchTree2">SearchTree2</a> [module, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.Abs">SearchTree2.Abs</a> [inductive, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.Abs_E">SearchTree2.Abs_E</a> [constructor, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.Abs_T">SearchTree2.Abs_T</a> [constructor, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.combine">SearchTree2.combine</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.E">SearchTree2.E</a> [constructor, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.elements">SearchTree2.elements</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.elements'">SearchTree2.elements'</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.empty_tree">SearchTree2.empty_tree</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.empty_tree_relate">SearchTree2.empty_tree_relate</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.insert">SearchTree2.insert</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.insert_relate">SearchTree2.insert_relate</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.key">SearchTree2.key</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.lookup">SearchTree2.lookup</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.lookup_relate">SearchTree2.lookup_relate</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.T">SearchTree2.T</a> [constructor, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.tree">SearchTree2.tree</a> [inductive, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.TREES">SearchTree2.TREES</a> [section, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.TREES.default">SearchTree2.TREES.default</a> [variable, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.TREES.V">SearchTree2.TREES.V</a> [variable, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.unrealistically_strong_can_relate">SearchTree2.unrealistically_strong_can_relate</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1">SectionExample1</a> [module, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.empty">SectionExample1.empty</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.lookup">SectionExample1.lookup</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.lookup_empty">SectionExample1.lookup_empty</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.mymap">SectionExample1.mymap</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2">SectionExample2</a> [module, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.empty">SectionExample2.empty</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.lookup">SectionExample2.lookup</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.lookup_empty">SectionExample2.lookup_empty</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.MAPS">SectionExample2.MAPS</a> [section, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.MAPS.default">SectionExample2.MAPS.default</a> [variable, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.MAPS.V">SectionExample2.MAPS.V</a> [variable, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.mymap">SectionExample2.mymap</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Selection.html#select">select</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="Selection.html">Selection</a> [library]<br/>
<a href="VFA.Selection.html#selection_sort">selection_sort</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_correct">selection_sort_correct</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_is_correct">selection_sort_is_correct</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_perm">selection_sort_perm</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_sorted">selection_sort_sorted</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_sorted_aux">selection_sort_sorted_aux</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#select_perm">select_perm</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#select_smallest">select_smallest</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#select_smallest_aux">select_smallest_aux</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Color.html#select_terminates">select_terminates</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Selection.html#selsort">selsort</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selsort'_perm">selsort'_perm</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selsort_perm">selsort_perm</a> [lemma, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Multiset.html#singleton">singleton</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Color.html#Sin_domain">Sin_domain</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#sixlist">sixlist</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.SearchTree.html#slow_elements">slow_elements</a> [definition, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#slow_elements_range">slow_elements_range</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#Snot_in_empty">Snot_in_empty</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Sort.html#sort">sort</a> [definition, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="Sort.html">Sort</a> [library]<br/>
<a href="VFA.Selection.html#sorted">sorted</a> [inductive, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Sort.html#sorted">sorted</a> [inductive, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sorted'">sorted'</a> [definition, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sorted'_sorted">sorted'_sorted</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#sorted_cons">sorted_cons</a> [constructor, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Sort.html#sorted_cons">sorted_cons</a> [constructor, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Color.html#Sorted_lt_key">Sorted_lt_key</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Sort.html#sorted_nil">sorted_nil</a> [constructor, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#sorted_nil">sorted_nil</a> [constructor, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Sort.html#sorted_sorted'">sorted_sorted'</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sorted_1">sorted_1</a> [constructor, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#sorted_1">sorted_1</a> [constructor, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Color.html#SortE_equivlistE_eqlistE">SortE_equivlistE_eqlistE</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Extract.html#Sort1">Sort1</a> [module, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Sort1.insert">Sort1.insert</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Sort1.sort">Sort1.sort</a> [definition, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Multiset.html#sort_contents">sort_contents</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Sort.html#sort_perm">sort_perm</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#sort_pi">sort_pi</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Multiset.html#sort_pi">sort_pi</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Sort.html#sort_pi">sort_pi</a> [definition, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Multiset.html#sort_pi_same_contents">sort_pi_same_contents</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Sort.html#sort_sorted">sort_sorted</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sort_sorted'">sort_sorted'</a> [lemma, in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Multiset.html#sort_specifications_equivalent">sort_specifications_equivalent</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Color.html#specialize_SortA_equivlistA_eqlistA">specialize_SortA_equivlistA_eqlistA</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Sremove_cardinal_less">Sremove_cardinal_less</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Sremove_elements">Sremove_elements</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Sremove_elements">Sremove_elements</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#step">step</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#stepish">stepish</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#step_relate">step_relate</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Redblack.html#ST_E">ST_E</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#ST_E">ST_E</a> [constructor, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#ST_intro">ST_intro</a> [constructor, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#ST_intro">ST_intro</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ST_T">ST_T</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#ST_T">ST_T</a> [constructor, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#subset_nodes">subset_nodes</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#subset_nodes_sub">subset_nodes_sub</a> [lemma, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="global_T"></a><h2>T </h2>
<a href="VFA.Redblack.html#T">T</a> [constructor, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#T">T</a> [constructor, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.ADT.html#TABLE">TABLE</a> [module, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.default">TABLE.default</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.empty">TABLE.empty</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.gempty">TABLE.gempty</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.get">TABLE.get</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.gso">TABLE.gso</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.gss">TABLE.gss</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.key">TABLE.key</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.set">TABLE.set</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.table">TABLE.table</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.V">TABLE.V</a> [axiom, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Decide.html#three_less_seven_1">three_less_seven_1</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#three_less_seven_2">three_less_seven_2</a> [lemma, in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Trie.html#three_ten">three_ten</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Selection.html#too_much_gas">too_much_gas</a> [definition, in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Redblack.html#tree">tree</a> [inductive, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#tree">tree</a> [inductive, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#TREES">TREES</a> [section, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#TREES">TREES</a> [section, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#TREES.default">TREES.default</a> [variable, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#TREES.default">TREES.default</a> [variable, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES">TREES.EXAMPLES</a> [section, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES.v2">TREES.EXAMPLES.v2</a> [variable, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES.v4">TREES.EXAMPLES.v4</a> [variable, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES.v5">TREES.EXAMPLES.v5</a> [variable, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#TREES.V">TREES.V</a> [variable, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#TREES.V">TREES.V</a> [variable, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.ADT.html#TreeTable">TreeTable</a> [module, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.default">TreeTable.default</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.empty">TreeTable.empty</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.gempty">TreeTable.gempty</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.get">TreeTable.get</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.gso">TreeTable.gso</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.gss">TreeTable.gss</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.key">TreeTable.key</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.set">TreeTable.set</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.table">TreeTable.table</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.V">TreeTable.V</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2">TreeTable2</a> [module, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.default">TreeTable2.default</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.empty">TreeTable2.empty</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.gempty">TreeTable2.gempty</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.get">TreeTable2.get</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.gso">TreeTable2.gso</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.gss">TreeTable2.gss</a> [lemma, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.key">TreeTable2.key</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.set">TreeTable2.set</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.table">TreeTable2.table</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.V">TreeTable2.V</a> [definition, in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Trie.html#trie">trie</a> [inductive, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="Trie.html">Trie</a> [library]<br/>
<a href="VFA.Trie.html#trie_table">trie_table</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#T_neq_E">T_neq_E</a> [lemma, in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="global_U"></a><h2>U </h2>
<a href="VFA.Color.html#undirected">undirected</a> [definition, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Multiset.html#union">union</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#union_assoc">union_assoc</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#union_comm">union_comm</a> [lemma, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.SearchTree.html#unrealistically_strong_can_relate">unrealistically_strong_can_relate</a> [lemma, in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="global_V"></a><h2>V </h2>
<a href="VFA.Multiset.html#value">value</a> [definition, in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#VerySlow">VerySlow</a> [module, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#VerySlow.collisions">VerySlow.collisions</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#VerySlow.collisions_pi">VerySlow.collisions_pi</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#VerySlow.loop">VerySlow.loop</a> [definition, in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="global_W"></a><h2>W </h2>
<a href="VFA.Color.html#WF">WF</a> [module, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#WP">WP</a> [module, in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="global_Z"></a><h2>Z </h2>
<a href="VFA.Extract.html#Z_eqb_reflect">Z_eqb_reflect</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Z_ltb_reflect">Z_ltb_reflect</a> [lemma, in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<br/><br/><a name="global_:"></a><h2>: </h2>
<a href="VFA.Perm.html#::nat_scope:x_'>=?'_x">::nat_scope:x_'>=?'_x</a> [notation, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#::nat_scope:x_'>?'_x">::nat_scope:x_'>?'_x</a> [notation, in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<br/><br/><hr/>
<h1>Notation Index</h1>
<a name="notation_I"></a><h2>I </h2>
<a href="VFA.Trie.html#Integers.:::x_'~'_'0'">Integers.:::x_'~'_'0'</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.:::x_'~'_'1'">Integers.:::x_'~'_'1'</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="notation_S"></a><h2>S </h2>
<a href="VFA.Decide.html#ScratchPad.::type_scope:'{'_x_'}'_'+'_'{'_x_'}'">ScratchPad.::type_scope:'{'_x_'}'_'+'_'{'_x_'}'</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<br/><br/><a name="notation_:"></a><h2>: </h2>
<a href="VFA.Perm.html#::nat_scope:x_'>=?'_x">::nat_scope:x_'>=?'_x</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#::nat_scope:x_'>?'_x">::nat_scope:x_'>?'_x</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<br/><br/><hr/>
<h1>Module Index</h1>
<a name="module_B"></a><h2>B </h2>
<a href="VFA.Binom.html#BinomQueue">BinomQueue</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<br/><br/><a name="module_E"></a><h2>E </h2>
<a href="VFA.Color.html#E">E</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Extract.html#Experiments">Experiments</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Perm.html#Exploration1">Exploration1</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<br/><br/><a name="module_F"></a><h2>F </h2>
<a href="VFA.Trie.html#FastEnough">FastEnough</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="module_I"></a><h2>I </h2>
<a href="VFA.Trie.html#Integers">Integers</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Extract.html#IntMaps">IntMaps</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<br/><br/><a name="module_L"></a><h2>L </h2>
<a href="VFA.ADT.html#L">L</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH">LISTISH</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue">List_Priqueue</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<br/><br/><a name="module_M"></a><h2>M </h2>
<a href="VFA.Color.html#M">M</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#MapsTable">MapsTable</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="module_P"></a><h2>P </h2>
<a href="VFA.Priqueue.html#PRIQUEUE">PRIQUEUE</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<br/><br/><a name="module_R"></a><h2>R </h2>
<a href="VFA.Trie.html#RatherSlow">RatherSlow</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="module_S"></a><h2>S </h2>
<a href="VFA.Color.html#S">S</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Decide.html#ScratchPad">ScratchPad</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2">ScratchPad2</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Extract.html#SearchTree2">SearchTree2</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1">SectionExample1</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2">SectionExample2</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Extract.html#Sort1">Sort1</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<br/><br/><a name="module_T"></a><h2>T </h2>
<a href="VFA.ADT.html#TABLE">TABLE</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable">TreeTable</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2">TreeTable2</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="module_V"></a><h2>V </h2>
<a href="VFA.Trie.html#VerySlow">VerySlow</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="module_W"></a><h2>W </h2>
<a href="VFA.Color.html#WF">WF</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#WP">WP</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><hr/>
<h1>Variable Index</h1>
<a name="variable_A"></a><h2>A </h2>
<a href="VFA.ADT.html#ADT_SUMMARY.default">ADT_SUMMARY.default</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#ADT_SUMMARY.V">ADT_SUMMARY.V</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="variable_S"></a><h2>S </h2>
<a href="VFA.Extract.html#SearchTree2.TREES.default">SearchTree2.TREES.default</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.TREES.V">SearchTree2.TREES.V</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.MAPS.default">SectionExample2.MAPS.default</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.MAPS.V">SectionExample2.MAPS.V</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="variable_T"></a><h2>T </h2>
<a href="VFA.SearchTree.html#TREES.default">TREES.default</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#TREES.default">TREES.default</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES.v2">TREES.EXAMPLES.v2</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES.v4">TREES.EXAMPLES.v4</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES.v5">TREES.EXAMPLES.v5</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#TREES.V">TREES.V</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#TREES.V">TREES.V</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><hr/>
<h1>Library Index</h1>
<a name="library_A"></a><h2>A </h2>
<a href="ADT.html">ADT</a> <br/>
<br/><br/><a name="library_B"></a><h2>B </h2>
<a href="Binom.html">Binom</a> <br/>
<br/><br/><a name="library_C"></a><h2>C </h2>
<a href="Color.html">Color</a> <br/>
<br/><br/><a name="library_D"></a><h2>D </h2>
<a href="Decide.html">Decide</a> <br/>
<br/><br/><a name="library_E"></a><h2>E </h2>
<a href="Extract.html">Extract</a> <br/>
<br/><br/><a name="library_M"></a><h2>M </h2>
<a href="Multiset.html">Multiset</a> <br/>
<br/><br/><a name="library_P"></a><h2>P </h2>
<a href="Perm.html">Perm</a> <br/>
<a href="Preface.html">Preface</a> <br/>
<a href="Priqueue.html">Priqueue</a> <br/>
<br/><br/><a name="library_R"></a><h2>R </h2>
<a href="Redblack.html">Redblack</a> <br/>
<br/><br/><a name="library_S"></a><h2>S </h2>
<a href="SearchTree.html">SearchTree</a> <br/>
<a href="Selection.html">Selection</a> <br/>
<a href="Sort.html">Sort</a> <br/>
<br/><br/><a name="library_T"></a><h2>T </h2>
<a href="Trie.html">Trie</a> <br/>
<br/><br/><hr/>
<h1>Lemma Index</h1>
<a name="lemma_A"></a><h2>A </h2>
<a href="VFA.SearchTree.html#abstraction_of_bogus_tree">abstraction_of_bogus_tree</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#Abs_helper">Abs_helper</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Color.html#adj_ext">adj_ext</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="lemma_B"></a><h2>B </h2>
<a href="VFA.Redblack.html#balance_relate">balance_relate</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#balance_SearchTree">balance_SearchTree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#balance_SearchTree">balance_SearchTree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#balance_SearchTree">balance_SearchTree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.abs_perm">BinomQueue.abs_perm</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.can_relate">BinomQueue.can_relate</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.carry_elems">BinomQueue.carry_elems</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.carry_valid">BinomQueue.carry_valid</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_None_relate">BinomQueue.delete_max_None_relate</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_Some_priq">BinomQueue.delete_max_Some_priq</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_Some_relate">BinomQueue.delete_max_Some_relate</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.empty_priq">BinomQueue.empty_priq</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.empty_relate">BinomQueue.empty_relate</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.insert_priq">BinomQueue.insert_priq</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.insert_relate">BinomQueue.insert_relate</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.join_elems">BinomQueue.join_elems</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.join_valid">BinomQueue.join_valid</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.merge_priq">BinomQueue.merge_priq</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.merge_relate">BinomQueue.merge_relate</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priqueue_elems_ext">BinomQueue.priqueue_elems_ext</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.smash_elems">BinomQueue.smash_elems</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.smash_valid">BinomQueue.smash_valid</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_can_relate">BinomQueue.tree_can_relate</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems_ext">BinomQueue.tree_elems_ext</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_perm">BinomQueue.tree_perm</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<br/><br/><a name="lemma_C"></a><h2>C </h2>
<a href="VFA.SearchTree.html#can_relate">can_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#cardinal_map">cardinal_map</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#check_example_map">check_example_map</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#check_too_clever">check_too_clever</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#color_correct">color_correct</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Decide.html#compute_with_lt_dec">compute_with_lt_dec</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#compute_with_StdLib_lt_dec">compute_with_StdLib_lt_dec</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.ADT.html#cons_relate">cons_relate</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Multiset.html#contents_in">contents_in</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#contents_perm">contents_perm</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#contents_perm_aux">contents_perm_aux</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.ADT.html#create_relate">create_relate</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="lemma_D"></a><h2>D </h2>
<a href="VFA.Multiset.html#delete_contents">delete_contents</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<br/><br/><a name="lemma_E"></a><h2>E </h2>
<a href="VFA.SearchTree.html#elements_relate">elements_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#elements_relate">elements_relate</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#elements_relate">elements_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#elements_relateX">elements_relateX</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#elements_relate_second_attempt">elements_relate_second_attempt</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#elements_slow_elements">elements_slow_elements</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#empty_is_trie">empty_is_trie</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#empty_relate">empty_relate</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#empty_tree_relate">empty_tree_relate</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#empty_tree_relate">empty_tree_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#empty_tree_SearchTree">empty_tree_SearchTree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#empty_tree_SearchTree">empty_tree_SearchTree</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Perm.html#eqb_reflect">eqb_reflect</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Color.html#eqlistA_Eeq_eq">eqlistA_Eeq_eq</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#example_SearchTree_bad">example_SearchTree_bad</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#example_SearchTree_good">example_SearchTree_good</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#expand_range_SearchTree'">expand_range_SearchTree'</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Perm.html#Exploration1.bogus_subtraction">Exploration1.bogus_subtraction</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_correct">Exploration1.maybe_swap_correct</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_idempotent">Exploration1.maybe_swap_idempotent</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_idempotent">Exploration1.maybe_swap_idempotent</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_idempotent'">Exploration1.maybe_swap_idempotent'</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_perm">Exploration1.maybe_swap_perm</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.omega_example1">Exploration1.omega_example1</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.omega_example1">Exploration1.omega_example1</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.omega_example2">Exploration1.omega_example2</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<br/><br/><a name="lemma_F"></a><h2>F </h2>
<a href="VFA.ADT.html#fibish_correct">fibish_correct</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Color.html#filter_sortE">filter_sortE</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#fold_right_rev_left">fold_right_rev_left</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Sort.html#Forall_nth">Forall_nth</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Perm.html#Forall_perm">Forall_perm</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<br/><br/><a name="lemma_I"></a><h2>I </h2>
<a href="VFA.Color.html#InA_map_fst_key">InA_map_fst_key</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Multiset.html#insertion_sort_correct">insertion_sort_correct</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Sort.html#insertion_sort_correct">insertion_sort_correct</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Multiset.html#insert_contents">insert_contents</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Redblack.html#insert_is_redblack">insert_is_redblack</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#insert_is_trie">insert_is_trie</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Sort.html#insert_perm">insert_perm</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Trie.html#insert_relate">insert_relate</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#insert_relate">insert_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#insert_relate">insert_relate</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#insert_relate'">insert_relate'</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#insert_SearchTree">insert_SearchTree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#insert_SearchTree">insert_SearchTree</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Sort.html#insert_sorted">insert_sorted</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#insert_sorted'">insert_sorted'</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Redblack.html#ins_is_redblack">ins_is_redblack</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_not_E">ins_not_E</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_not_E">ins_not_E</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_not_E">ins_not_E</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_relate">ins_relate</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ins_SearchTree">ins_SearchTree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#Integers.addc_correct">Integers.addc_correct</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.add_correct">Integers.add_correct</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.compare_correct">Integers.compare_correct</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.positive2nat_pos">Integers.positive2nat_pos</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.succ_correct">Integers.succ_correct</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update_eq">IntMaps.t_update_eq</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update_neq">IntMaps.t_update_neq</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update_shadow">IntMaps.t_update_shadow</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#int_ltb_reflect">int_ltb_reflect</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Color.html#in_colors_of_1">in_colors_of_1</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#In_decidable">In_decidable</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Multiset.html#in_perm_delete">in_perm_delete</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Redblack.html#is_redblack_toblack">is_redblack_toblack</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="lemma_L"></a><h2>L </h2>
<a href="VFA.Perm.html#leb_reflect">leb_reflect</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.SearchTree.html#list2map_app_left">list2map_app_left</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#list2map_app_right">list2map_app_right</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#list2map_not_in_default">list2map_not_in_default</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.abs_perm">List_Priqueue.abs_perm</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.can_relate">List_Priqueue.can_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max_None_relate">List_Priqueue.delete_max_None_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max_Some_priq">List_Priqueue.delete_max_Some_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max_Some_relate">List_Priqueue.delete_max_Some_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.empty_priq">List_Priqueue.empty_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.empty_relate">List_Priqueue.empty_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.insert_priq">List_Priqueue.insert_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.insert_relate">List_Priqueue.insert_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.merge_priq">List_Priqueue.merge_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.merge_relate">List_Priqueue.merge_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select_biggest">List_Priqueue.select_biggest</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select_biggest_aux">List_Priqueue.select_biggest_aux</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select_perm">List_Priqueue.select_perm</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Trie.html#lookup_relate">lookup_relate</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#lookup_relate">lookup_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#lookup_relate">lookup_relate</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#lookup_relateX">lookup_relateX</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#lookup_relate'">lookup_relate'</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#look_ins_other">look_ins_other</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#look_ins_same">look_ins_same</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#look_leaf">look_leaf</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Perm.html#ltb_reflect">ltb_reflect</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Color.html#lt_proper">lt_proper</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#lt_strict">lt_strict</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="lemma_M"></a><h2>M </h2>
<a href="VFA.Redblack.html#makeblack_fiddle">makeblack_fiddle</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#makeBlack_relate">makeBlack_relate</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.ADT.html#MapsTable.gempty">MapsTable.gempty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.gso">MapsTable.gso</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.gss">MapsTable.gss</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Color.html#Mremove_cardinal_less">Mremove_cardinal_less</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Mremove_elements">Mremove_elements</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="lemma_N"></a><h2>N </h2>
<a href="VFA.SearchTree.html#naive_lookup_relateX">naive_lookup_relateX</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#nat2pos2nat">nat2pos2nat</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#nat2pos_injective">nat2pos_injective</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#not_elements_relate">not_elements_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#not_naive_lookup_relateX">not_naive_lookup_relateX</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.ADT.html#nth_firstn">nth_firstn</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#nth_relate">nth_relate</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="lemma_P"></a><h2>P </h2>
<a href="VFA.Multiset.html#perm_contents">perm_contents</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#pos2nat2pos">pos2nat2pos</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#pos2nat_injective">pos2nat_injective</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Color.html#Proper_eq_eq">Proper_eq_eq</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Proper_eq_key_elt">Proper_eq_key_elt</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="lemma_R"></a><h2>R </h2>
<a href="VFA.ADT.html#repeat_step_relate">repeat_step_relate</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="lemma_S"></a><h2>S </h2>
<a href="VFA.Multiset.html#same_contents_iff_perm">same_contents_iff_perm</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.greater23">ScratchPad.greater23</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.less37">ScratchPad.less37</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.lt_dec_equivalent">ScratchPad.lt_dec_equivalent</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.insert_sorted">ScratchPad2.insert_sorted</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.prove_with_max_axiom">ScratchPad2.prove_with_max_axiom</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Redblack.html#SearchTree'_le">SearchTree'_le</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#SearchTree'_le">SearchTree'_le</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.empty_tree_relate">SearchTree2.empty_tree_relate</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.insert_relate">SearchTree2.insert_relate</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.lookup_relate">SearchTree2.lookup_relate</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.unrealistically_strong_can_relate">SearchTree2.unrealistically_strong_can_relate</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.lookup_empty">SectionExample1.lookup_empty</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.lookup_empty">SectionExample2.lookup_empty</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Selection.html#selection_sort_is_correct">selection_sort_is_correct</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_perm">selection_sort_perm</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_sorted">selection_sort_sorted</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_sorted_aux">selection_sort_sorted_aux</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#select_perm">select_perm</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#select_smallest">select_smallest</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#select_smallest_aux">select_smallest_aux</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Color.html#select_terminates">select_terminates</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Selection.html#selsort'_perm">selsort'_perm</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selsort_perm">selsort_perm</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Color.html#Sin_domain">Sin_domain</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#slow_elements_range">slow_elements_range</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#Snot_in_empty">Snot_in_empty</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Sort.html#sorted'_sorted">sorted'_sorted</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Color.html#Sorted_lt_key">Sorted_lt_key</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Sort.html#sorted_sorted'">sorted_sorted'</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Color.html#SortE_equivlistE_eqlistE">SortE_equivlistE_eqlistE</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Multiset.html#sort_contents">sort_contents</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Sort.html#sort_perm">sort_perm</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sort_sorted">sort_sorted</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sort_sorted'">sort_sorted'</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Multiset.html#sort_specifications_equivalent">sort_specifications_equivalent</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Color.html#specialize_SortA_equivlistA_eqlistA">specialize_SortA_equivlistA_eqlistA</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Sremove_cardinal_less">Sremove_cardinal_less</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Sremove_elements">Sremove_elements</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#Sremove_elements">Sremove_elements</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#step_relate">step_relate</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Color.html#subset_nodes_sub">subset_nodes_sub</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="lemma_T"></a><h2>T </h2>
<a href="VFA.Decide.html#three_less_seven_1">three_less_seven_1</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#three_less_seven_2">three_less_seven_2</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.ADT.html#TreeTable.gempty">TreeTable.gempty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.gso">TreeTable.gso</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.gss">TreeTable.gss</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.gempty">TreeTable2.gempty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.gso">TreeTable2.gso</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.gss">TreeTable2.gss</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Redblack.html#T_neq_E">T_neq_E</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="lemma_U"></a><h2>U </h2>
<a href="VFA.Multiset.html#union_assoc">union_assoc</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#union_comm">union_comm</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.SearchTree.html#unrealistically_strong_can_relate">unrealistically_strong_can_relate</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="lemma_Z"></a><h2>Z </h2>
<a href="VFA.Extract.html#Z_eqb_reflect">Z_eqb_reflect</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Z_ltb_reflect">Z_ltb_reflect</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<br/><br/><hr/>
<h1>Axiom Index</h1>
<a name="axiom_I"></a><h2>I </h2>
<a href="VFA.Extract.html#int">int</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#int2Z">int2Z</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<br/><br/><a name="axiom_L"></a><h2>L </h2>
<a href="VFA.ADT.html#LISTISH.cons">LISTISH.cons</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH.create">LISTISH.create</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH.list">LISTISH.list</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#LISTISH.nth">LISTISH.nth</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Extract.html#ltb">ltb</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#ltb_lt">ltb_lt</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<br/><br/><a name="axiom_P"></a><h2>P </h2>
<a href="VFA.Priqueue.html#PRIQUEUE.Abs">PRIQUEUE.Abs</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.abs_perm">PRIQUEUE.abs_perm</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.can_relate">PRIQUEUE.can_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max">PRIQUEUE.delete_max</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max_None_relate">PRIQUEUE.delete_max_None_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max_Some_priq">PRIQUEUE.delete_max_Some_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.delete_max_Some_relate">PRIQUEUE.delete_max_Some_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.empty">PRIQUEUE.empty</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.empty_priq">PRIQUEUE.empty_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.empty_relate">PRIQUEUE.empty_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.insert">PRIQUEUE.insert</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.insert_priq">PRIQUEUE.insert_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.insert_relate">PRIQUEUE.insert_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.merge">PRIQUEUE.merge</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.merge_priq">PRIQUEUE.merge_priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.merge_relate">PRIQUEUE.merge_relate</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.priq">PRIQUEUE.priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.priqueue">PRIQUEUE.priqueue</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<br/><br/><a name="axiom_S"></a><h2>S </h2>
<a href="VFA.Decide.html#ScratchPad2.lt_dec_axiom_1">ScratchPad2.lt_dec_axiom_1</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.lt_dec_axiom_2">ScratchPad2.lt_dec_axiom_2</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<br/><br/><a name="axiom_T"></a><h2>T </h2>
<a href="VFA.ADT.html#TABLE.default">TABLE.default</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.empty">TABLE.empty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.gempty">TABLE.gempty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.get">TABLE.get</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.gso">TABLE.gso</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.gss">TABLE.gss</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.set">TABLE.set</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.table">TABLE.table</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TABLE.V">TABLE.V</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><hr/>
<h1>Constructor Index</h1>
<a name="constructor_A"></a><h2>A </h2>
<a href="VFA.Redblack.html#Abs_E">Abs_E</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#Abs_E">Abs_E</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#Abs_T">Abs_T</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#Abs_T">Abs_T</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="constructor_B"></a><h2>B </h2>
<a href="VFA.Binom.html#BinomQueue.Leaf">BinomQueue.Leaf</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.Node">BinomQueue.Node</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems_leaf">BinomQueue.tree_elems_leaf</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems_node">BinomQueue.tree_elems_node</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Redblack.html#Black">Black</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="constructor_E"></a><h2>E </h2>
<a href="VFA.SearchTree.html#E">E</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#E">E</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="constructor_I"></a><h2>I </h2>
<a href="VFA.Trie.html#Integers.Eq">Integers.Eq</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Gt">Integers.Gt</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Lt">Integers.Lt</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.xH">Integers.xH</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.xI">Integers.xI</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.xO">Integers.xO</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Zneg">Integers.Zneg</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Zpos">Integers.Zpos</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Z0">Integers.Z0</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#IsRB_b">IsRB_b</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#IsRB_leaf">IsRB_leaf</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#IsRB_r">IsRB_r</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="constructor_L"></a><h2>L </h2>
<a href="VFA.Trie.html#Leaf">Leaf</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.Abs_intro">List_Priqueue.Abs_intro</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<br/><br/><a name="constructor_N"></a><h2>N </h2>
<a href="VFA.Trie.html#Node">Node</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#nrRB_b">nrRB_b</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#nrRB_r">nrRB_r</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="constructor_R"></a><h2>R </h2>
<a href="VFA.Redblack.html#Red">Red</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="constructor_S"></a><h2>S </h2>
<a href="VFA.Decide.html#ScratchPad.left">ScratchPad.left</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.right">ScratchPad.right</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted_cons">ScratchPad2.sorted_cons</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted_nil">ScratchPad2.sorted_nil</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted_1">ScratchPad2.sorted_1</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.Abs_E">SearchTree2.Abs_E</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.Abs_T">SearchTree2.Abs_T</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.E">SearchTree2.E</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.T">SearchTree2.T</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Selection.html#sorted_cons">sorted_cons</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Sort.html#sorted_cons">sorted_cons</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sorted_nil">sorted_nil</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#sorted_nil">sorted_nil</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Sort.html#sorted_1">sorted_1</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#sorted_1">sorted_1</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Redblack.html#ST_E">ST_E</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#ST_E">ST_E</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#ST_intro">ST_intro</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#ST_intro">ST_intro</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#ST_T">ST_T</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#ST_T">ST_T</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="constructor_T"></a><h2>T </h2>
<a href="VFA.Redblack.html#T">T</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#T">T</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><hr/>
<h1>Inductive Index</h1>
<a name="inductive_A"></a><h2>A </h2>
<a href="VFA.SearchTree.html#Abs">Abs</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#Abs">Abs</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="inductive_B"></a><h2>B </h2>
<a href="VFA.Binom.html#BinomQueue.priqueue_elems">BinomQueue.priqueue_elems</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree">BinomQueue.tree</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.tree_elems">BinomQueue.tree_elems</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<br/><br/><a name="inductive_C"></a><h2>C </h2>
<a href="VFA.Redblack.html#color">color</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="inductive_I"></a><h2>I </h2>
<a href="VFA.Trie.html#Integers.comparison">Integers.comparison</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.positive">Integers.positive</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.Z">Integers.Z</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#is_redblack">is_redblack</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="inductive_L"></a><h2>L </h2>
<a href="VFA.Priqueue.html#List_Priqueue.Abs'">List_Priqueue.Abs'</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.ADT.html#L_Abs">L_Abs</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="inductive_N"></a><h2>N </h2>
<a href="VFA.Redblack.html#nearly_redblack">nearly_redblack</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="inductive_S"></a><h2>S </h2>
<a href="VFA.Decide.html#ScratchPad.sumbool">ScratchPad.sumbool</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sorted">ScratchPad2.sorted</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.SearchTree.html#SearchTree">SearchTree</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#SearchTree">SearchTree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Redblack.html#SearchTree'">SearchTree'</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#SearchTree'">SearchTree'</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.Abs">SearchTree2.Abs</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.tree">SearchTree2.tree</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Selection.html#sorted">sorted</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Sort.html#sorted">sorted</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<br/><br/><a name="inductive_T"></a><h2>T </h2>
<a href="VFA.Redblack.html#tree">tree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#tree">tree</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#trie">trie</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><hr/>
<h1>Section Index</h1>
<a name="section_A"></a><h2>A </h2>
<a href="VFA.ADT.html#ADT_SUMMARY">ADT_SUMMARY</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="section_S"></a><h2>S </h2>
<a href="VFA.Extract.html#SearchTree2.TREES">SearchTree2.TREES</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.MAPS">SectionExample2.MAPS</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="section_T"></a><h2>T </h2>
<a href="VFA.SearchTree.html#TREES">TREES</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#TREES">TREES</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#TREES.EXAMPLES">TREES.EXAMPLES</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><hr/>
<h1>Definition Index</h1>
<a name="definition_A"></a><h2>A </h2>
<a href="VFA.Trie.html#Abs">Abs</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#abstract">abstract</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#AbsX">AbsX</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#Abs_three_ten">Abs_three_ten</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Color.html#add_edge">add_edge</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#adj">adj</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="definition_B"></a><h2>B </h2>
<a href="VFA.Redblack.html#balance">balance</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.Abs">BinomQueue.Abs</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.carry">BinomQueue.carry</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max">BinomQueue.delete_max</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.delete_max_aux">BinomQueue.delete_max_aux</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.empty">BinomQueue.empty</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.find_max">BinomQueue.find_max</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.find_max'">BinomQueue.find_max'</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.heap_delete_max">BinomQueue.heap_delete_max</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.insert">BinomQueue.insert</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.join">BinomQueue.join</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.key">BinomQueue.key</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.manual_grade_for_priqueue_elems">BinomQueue.manual_grade_for_priqueue_elems</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.merge">BinomQueue.merge</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.pow2heap">BinomQueue.pow2heap</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.pow2heap'">BinomQueue.pow2heap'</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priq">BinomQueue.priq</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priqueue">BinomQueue.priqueue</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.priq'">BinomQueue.priq'</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.smash">BinomQueue.smash</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<a href="VFA.Binom.html#BinomQueue.unzip">BinomQueue.unzip</a> [in <a href="VFA.Binom.html">VFA.Binom</a>]<br/>
<br/><br/><a name="definition_C"></a><h2>C </h2>
<a href="VFA.Color.html#color">color</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#coloring">coloring</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#coloring_ok">coloring_ok</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#colors_of">colors_of</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#color1">color1</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Redblack.html#combine">combine</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#combine">combine</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Multiset.html#contents">contents</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<br/><br/><a name="definition_D"></a><h2>D </h2>
<a href="VFA.Color.html#domain_example_map">domain_example_map</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="definition_E"></a><h2>E </h2>
<a href="VFA.Redblack.html#elements">elements</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#elements">elements</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#elements'">elements'</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#elements'">elements'</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Redblack.html#elements_property">elements_property</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#empty">empty</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Multiset.html#empty">empty</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Redblack.html#empty_tree">empty_tree</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#empty_tree">empty_tree</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#equivlistA_example">equivlistA_example</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#example_map">example_map</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Color.html#example_map">example_map</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.SearchTree.html#example_tree">example_tree</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Extract.html#Experiments.E">Experiments.E</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.empty_tree">Experiments.empty_tree</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.insert">Experiments.insert</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.lookup">Experiments.lookup</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Experiments.T">Experiments.T</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Perm.html#Exploration1.butterfly">Exploration1.butterfly</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.first_le_second">Exploration1.first_le_second</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.manual_grade_for_Permutation_properties">Exploration1.manual_grade_for_Permutation_properties</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap">Exploration1.maybe_swap</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_123">Exploration1.maybe_swap_123</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.maybe_swap_321">Exploration1.maybe_swap_321</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.not_a_permutation">Exploration1.not_a_permutation</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#Exploration1.permut_example">Exploration1.permut_example</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<br/><br/><a name="definition_F"></a><h2>F </h2>
<a href="VFA.Trie.html#FastEnough.collisions">FastEnough.collisions</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#FastEnough.collisions_pi">FastEnough.collisions_pi</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#FastEnough.loop">FastEnough.loop</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.ADT.html#fib">fib</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#fibish">fibish</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#fibonacci">fibonacci</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.SearchTree.html#forall_nodes">forall_nodes</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="definition_G"></a><h2>G </h2>
<a href="VFA.Color.html#G">G</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#graph">graph</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="definition_H"></a><h2>H </h2>
<a href="VFA.Redblack.html#how_many_subgoals_remaining">how_many_subgoals_remaining</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<br/><br/><a name="definition_I"></a><h2>I </h2>
<a href="VFA.Color.html#InA_example">InA_example</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Redblack.html#ins">ins</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Trie.html#ins">ins</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.SearchTree.html#insert">insert</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#insert">insert</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#insert">insert</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.Sort.html#insert">insert</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Trie.html#Integers.add">Integers.add</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.addc">Integers.addc</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.compare">Integers.compare</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.positive2nat">Integers.positive2nat</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.print_in_binary">Integers.print_in_binary</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.succ">Integers.succ</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#Integers.ten">Integers.ten</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Extract.html#IntMaps.total_map">IntMaps.total_map</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_empty">IntMaps.t_empty</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#IntMaps.t_update">IntMaps.t_update</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Decide.html#in_4_pi">in_4_pi</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Sort.html#is_a_sorting_algorithm">is_a_sorting_algorithm</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Selection.html#is_a_sorting_algorithm">is_a_sorting_algorithm</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Multiset.html#is_a_sorting_algorithm'">is_a_sorting_algorithm'</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#is_trie">is_trie</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="definition_K"></a><h2>K </h2>
<a href="VFA.Redblack.html#key">key</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#key">key</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<br/><br/><a name="definition_L"></a><h2>L </h2>
<a href="VFA.SearchTree.html#list2map">list2map</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Multiset.html#list_delete">list_delete</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Decide.html#list_nat_eq_dec">list_nat_eq_dec</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#list_nat_in">list_nat_in</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.Abs">List_Priqueue.Abs</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.delete_max">List_Priqueue.delete_max</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.empty">List_Priqueue.empty</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.insert">List_Priqueue.insert</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.key">List_Priqueue.key</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.merge">List_Priqueue.merge</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.priq">List_Priqueue.priq</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.priqueue">List_Priqueue.priqueue</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Priqueue.html#List_Priqueue.select">List_Priqueue.select</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<a href="VFA.Trie.html#look">look</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Redblack.html#lookup">lookup</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#lookup">lookup</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Trie.html#lookup">lookup</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Color.html#low_deg">low_deg</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#L.cons">L.cons</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#L.create">L.create</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#L.list">L.list</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#L.nth">L.nth</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="definition_M"></a><h2>M </h2>
<a href="VFA.Redblack.html#makeBlack">makeBlack</a> [in <a href="VFA.Redblack.html">VFA.Redblack</a>]<br/>
<a href="VFA.SearchTree.html#manual_grade_for_elements_relate_informal">manual_grade_for_elements_relate_informal</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Multiset.html#manual_grade_for_permutations_vs_multiset">manual_grade_for_permutations_vs_multiset</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#manual_grade_for_successor_of_Z_constant_time">manual_grade_for_successor_of_Z_constant_time</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.ADT.html#MapsTable.default">MapsTable.default</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.empty">MapsTable.empty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.get">MapsTable.get</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.key">MapsTable.key</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.set">MapsTable.set</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.table">MapsTable.table</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#MapsTable.V">MapsTable.V</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Color.html#Mdomain">Mdomain</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#mk_graph">mk_graph</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Multiset.html#multiset">multiset</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Multiset.html#multiset_delete">multiset_delete</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<br/><br/><a name="definition_N"></a><h2>N </h2>
<a href="VFA.Trie.html#nat2pos">nat2pos</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Color.html#node">node</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#nodemap">nodemap</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#nodes">nodes</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#nodeset">nodeset</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Color.html#no_selfloop">no_selfloop</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="definition_O"></a><h2>O </h2>
<a href="VFA.Selection.html#out_of_gas">out_of_gas</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.ADT.html#O_Abs">O_Abs</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="definition_P"></a><h2>P </h2>
<a href="VFA.Color.html#palette">palette</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Trie.html#pos2nat">pos2nat</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Priqueue.html#PRIQUEUE.key">PRIQUEUE.key</a> [in <a href="VFA.Priqueue.html">VFA.Priqueue</a>]<br/>
<br/><br/><a name="definition_R"></a><h2>R </h2>
<a href="VFA.Trie.html#RatherSlow.collisions">RatherSlow.collisions</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.collisions_pi">RatherSlow.collisions_pi</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.empty">RatherSlow.empty</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.loop">RatherSlow.loop</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.total_mapz">RatherSlow.total_mapz</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#RatherSlow.update">RatherSlow.update</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Perm.html#reflect_example1">reflect_example1</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Perm.html#reflect_example2">reflect_example2</a> [in <a href="VFA.Perm.html">VFA.Perm</a>]<br/>
<a href="VFA.Color.html#remove_node">remove_node</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.ADT.html#repeat">repeat</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<br/><br/><a name="definition_S"></a><h2>S </h2>
<a href="VFA.Color.html#same_mod_10">same_mod_10</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.is_3_less_7">ScratchPad.is_3_less_7</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.lt_dec">ScratchPad.lt_dec</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.lt_dec'">ScratchPad.lt_dec'</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.t1">ScratchPad.t1</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.t2">ScratchPad.t2</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.t4">ScratchPad.t4</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v1a">ScratchPad.v1a</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v1b">ScratchPad.v1b</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v2a">ScratchPad.v2a</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad.v3">ScratchPad.v3</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.insert">ScratchPad2.insert</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.le_dec">ScratchPad2.le_dec</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.lt_dec">ScratchPad2.lt_dec</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.max_with_axiom">ScratchPad2.max_with_axiom</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.Decide.html#ScratchPad2.sort">ScratchPad2.sort</a> [in <a href="VFA.Decide.html">VFA.Decide</a>]<br/>
<a href="VFA.SearchTree.html#SearchTreeX">SearchTreeX</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.combine">SearchTree2.combine</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.elements">SearchTree2.elements</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.elements'">SearchTree2.elements'</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.empty_tree">SearchTree2.empty_tree</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.insert">SearchTree2.insert</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.key">SearchTree2.key</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#SearchTree2.lookup">SearchTree2.lookup</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.empty">SectionExample1.empty</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.lookup">SectionExample1.lookup</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample1.mymap">SectionExample1.mymap</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.empty">SectionExample2.empty</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.lookup">SectionExample2.lookup</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.SearchTree.html#SectionExample2.mymap">SectionExample2.mymap</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Selection.html#select">select</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort">selection_sort</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selection_sort_correct">selection_sort_correct</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Selection.html#selsort">selsort</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Multiset.html#singleton">singleton</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.ADT.html#sixlist">sixlist</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.SearchTree.html#slow_elements">slow_elements</a> [in <a href="VFA.SearchTree.html">VFA.SearchTree</a>]<br/>
<a href="VFA.Sort.html#sort">sort</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Sort.html#sorted'">sorted'</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Extract.html#Sort1.insert">Sort1.insert</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Extract.html#Sort1.sort">Sort1.sort</a> [in <a href="VFA.Extract.html">VFA.Extract</a>]<br/>
<a href="VFA.Selection.html#sort_pi">sort_pi</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.Multiset.html#sort_pi">sort_pi</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Sort.html#sort_pi">sort_pi</a> [in <a href="VFA.Sort.html">VFA.Sort</a>]<br/>
<a href="VFA.Multiset.html#sort_pi_same_contents">sort_pi_same_contents</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.ADT.html#step">step</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#stepish">stepish</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Color.html#subset_nodes">subset_nodes</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<br/><br/><a name="definition_T"></a><h2>T </h2>
<a href="VFA.ADT.html#TABLE.key">TABLE.key</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Trie.html#three_ten">three_ten</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Selection.html#too_much_gas">too_much_gas</a> [in <a href="VFA.Selection.html">VFA.Selection</a>]<br/>
<a href="VFA.ADT.html#TreeTable.default">TreeTable.default</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.empty">TreeTable.empty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.get">TreeTable.get</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.key">TreeTable.key</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.set">TreeTable.set</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.table">TreeTable.table</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable.V">TreeTable.V</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.default">TreeTable2.default</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.empty">TreeTable2.empty</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.get">TreeTable2.get</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.key">TreeTable2.key</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.set">TreeTable2.set</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.table">TreeTable2.table</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.ADT.html#TreeTable2.V">TreeTable2.V</a> [in <a href="VFA.ADT.html">VFA.ADT</a>]<br/>
<a href="VFA.Trie.html#trie_table">trie_table</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><a name="definition_U"></a><h2>U </h2>
<a href="VFA.Color.html#undirected">undirected</a> [in <a href="VFA.Color.html">VFA.Color</a>]<br/>
<a href="VFA.Multiset.html#union">union</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<br/><br/><a name="definition_V"></a><h2>V </h2>
<a href="VFA.Multiset.html#value">value</a> [in <a href="VFA.Multiset.html">VFA.Multiset</a>]<br/>
<a href="VFA.Trie.html#VerySlow.collisions">VerySlow.collisions</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#VerySlow.collisions_pi">VerySlow.collisions_pi</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<a href="VFA.Trie.html#VerySlow.loop">VerySlow.loop</a> [in <a href="VFA.Trie.html">VFA.Trie</a>]<br/>
<br/><br/><hr/><table>
<tr>
<td>Global Index</td>
<td><a href="coqindex.html#global_A">A</a></td>
<td><a href="coqindex.html#global_B">B</a></td>
<td><a href="coqindex.html#global_C">C</a></td>
<td><a href="coqindex.html#global_D">D</a></td>
<td><a href="coqindex.html#global_E">E</a></td>
<td><a href="coqindex.html#global_F">F</a></td>
<td><a href="coqindex.html#global_G">G</a></td>
<td><a href="coqindex.html#global_H">H</a></td>
<td><a href="coqindex.html#global_I">I</a></td>
<td>J</td>
<td><a href="coqindex.html#global_K">K</a></td>
<td><a href="coqindex.html#global_L">L</a></td>
<td><a href="coqindex.html#global_M">M</a></td>
<td><a href="coqindex.html#global_N">N</a></td>
<td><a href="coqindex.html#global_O">O</a></td>
<td><a href="coqindex.html#global_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#global_R">R</a></td>
<td><a href="coqindex.html#global_S">S</a></td>
<td><a href="coqindex.html#global_T">T</a></td>
<td><a href="coqindex.html#global_U">U</a></td>
<td><a href="coqindex.html#global_V">V</a></td>
<td><a href="coqindex.html#global_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="coqindex.html#global_Z">Z</a></td>
<td><a href="coqindex.html#global_:">:</a></td>
<td>_</td>
<td>(617 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#notation_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#notation_S">S</a></td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td><a href="coqindex.html#notation_:">:</a></td>
<td>_</td>
<td>(5 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td>A</td>
<td><a href="coqindex.html#module_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="coqindex.html#module_E">E</a></td>
<td><a href="coqindex.html#module_F">F</a></td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#module_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#module_L">L</a></td>
<td><a href="coqindex.html#module_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="coqindex.html#module_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#module_R">R</a></td>
<td><a href="coqindex.html#module_S">S</a></td>
<td><a href="coqindex.html#module_T">T</a></td>
<td>U</td>
<td><a href="coqindex.html#module_V">V</a></td>
<td><a href="coqindex.html#module_W">W</a></td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(27 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
<td><a href="coqindex.html#variable_A">A</a></td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#variable_S">S</a></td>
<td><a href="coqindex.html#variable_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(13 entries)</td>
</tr>
<tr>
<td>Library Index</td>
<td><a href="coqindex.html#library_A">A</a></td>
<td><a href="coqindex.html#library_B">B</a></td>
<td><a href="coqindex.html#library_C">C</a></td>
<td><a href="coqindex.html#library_D">D</a></td>
<td><a href="coqindex.html#library_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="coqindex.html#library_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="coqindex.html#library_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#library_R">R</a></td>
<td><a href="coqindex.html#library_S">S</a></td>
<td><a href="coqindex.html#library_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(14 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
<td><a href="coqindex.html#lemma_A">A</a></td>
<td><a href="coqindex.html#lemma_B">B</a></td>
<td><a href="coqindex.html#lemma_C">C</a></td>
<td><a href="coqindex.html#lemma_D">D</a></td>
<td><a href="coqindex.html#lemma_E">E</a></td>
<td><a href="coqindex.html#lemma_F">F</a></td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#lemma_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#lemma_L">L</a></td>
<td><a href="coqindex.html#lemma_M">M</a></td>
<td><a href="coqindex.html#lemma_N">N</a></td>
<td>O</td>
<td><a href="coqindex.html#lemma_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#lemma_R">R</a></td>
<td><a href="coqindex.html#lemma_S">S</a></td>
<td><a href="coqindex.html#lemma_T">T</a></td>
<td><a href="coqindex.html#lemma_U">U</a></td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="coqindex.html#lemma_Z">Z</a></td>
<td>_</td>
<td>(211 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#axiom_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#axiom_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td><a href="coqindex.html#axiom_P">P</a></td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#axiom_S">S</a></td>
<td><a href="coqindex.html#axiom_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(37 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
<td><a href="coqindex.html#constructor_A">A</a></td>
<td><a href="coqindex.html#constructor_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="coqindex.html#constructor_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#constructor_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#constructor_L">L</a></td>
<td>M</td>
<td><a href="coqindex.html#constructor_N">N</a></td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td><a href="coqindex.html#constructor_R">R</a></td>
<td><a href="coqindex.html#constructor_S">S</a></td>
<td><a href="coqindex.html#constructor_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(52 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
<td><a href="coqindex.html#inductive_A">A</a></td>
<td><a href="coqindex.html#inductive_B">B</a></td>
<td><a href="coqindex.html#inductive_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="coqindex.html#inductive_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="coqindex.html#inductive_L">L</a></td>
<td>M</td>
<td><a href="coqindex.html#inductive_N">N</a></td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#inductive_S">S</a></td>
<td><a href="coqindex.html#inductive_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(26 entries)</td>
</tr>
<tr>
<td>Section Index</td>
<td><a href="coqindex.html#section_A">A</a></td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td>I</td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td><a href="coqindex.html#section_S">S</a></td>
<td><a href="coqindex.html#section_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(6 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
<td><a href="coqindex.html#definition_A">A</a></td>
<td><a href="coqindex.html#definition_B">B</a></td>
<td><a href="coqindex.html#definition_C">C</a></td>
<td><a href="coqindex.html#definition_D">D</a></td>
<td><a href="coqindex.html#definition_E">E</a></td>
<td><a href="coqindex.html#definition_F">F</a></td>
<td><a href="coqindex.html#definition_G">G</a></td>
<td><a href="coqindex.html#definition_H">H</a></td>
<td><a href="coqindex.html#definition_I">I</a></td>
<td>J</td>
<td><a href="coqindex.html#definition_K">K</a></td>
<td><a href="coqindex.html#definition_L">L</a></td>
<td><a href="coqindex.html#definition_M">M</a></td>
<td><a href="coqindex.html#definition_N">N</a></td>
<td><a href="coqindex.html#definition_O">O</a></td>
<td><a href="coqindex.html#definition_P">P</a></td>
<td>Q</td>
<td><a href="coqindex.html#definition_R">R</a></td>
<td><a href="coqindex.html#definition_S">S</a></td>
<td><a href="coqindex.html#definition_T">T</a></td>
<td><a href="coqindex.html#definition_U">U</a></td>
<td><a href="coqindex.html#definition_V">V</a></td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>(226 entries)</td>
</tr>
</table>
</div>

</div>

</body>
</html>